A:Type, B1,B2:(AType), eq:EqDecider(A), f:fpf(A; a.B1(a)), g:fpf(A; a.B2(a)).
fpf-sub(A; a.B1(a); eq; f; fpf-join(eq; f; g)) 

latex

Definitions	x:A. B(x), x(s), fpf-sub(A; a.B(a); eq; f; g), P  Q, A c B, P  Q, P  Q, P  Q, t  T, x. t(x), P  Q, prop{i:l}
Lemmas	fpf-join-dom2, fpf-trivial-subtype-top, assert wf, fpf-dom wf, fpf-ap wf, fpf-join-ap-left, fpf wf, deq wf